$\forall$${\it the\_es}$:ES, ${\it e'}$, $e$:E.
\\[0ex]($e$ $\in$ before(${\it e'}$)) $\Rightarrow$ ($\exists$$l$:E List. before(${\it e'}$) $=$ (before($e$) @ [$e$] @ $l$) $\in$ E List)